Inference at * 1 2 0 
Iof proof for Lemma iff preserves decidability:



1. A : 
2. B : 
3. A
4. A  B
  B  (B) 

latex

 by PERMUTE{1:n, 2:n, 2:n} 

latex

 1: 

 1: 5. B
 1:   False
 2: .....wf..... NILNIL

 2:   B  
 .

Definitions

t  T, Type, s = t, x:AB(x), False, left + right, P  Q, , P  Q, P  Q, A